(set-option :incremental false)
(set-info :source "The benchmarks come from Bounded Model Checking of software.
Contributed by Lorenzo Platania (c1009@unige.it).")
(set-info :status unknown)
(set-info :difficulty "unknown")
(set-info :category "industrial")
(set-logic QF_AUFBV)
(declare-fun main_0_head_0 () (_ BitVec 32))
(declare-fun main_0_head_1 () (_ BitVec 32))
(declare-fun arr_val_0 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_val_1 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_0 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_1 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_0 () (_ BitVec 32))
(declare-fun main_0_curr_1 () (_ BitVec 32))
(declare-fun main_0_i_0 () (_ BitVec 32))
(declare-fun main_0_i_1 () (_ BitVec 32))
(declare-fun main_0_tmp_0 () (_ BitVec 32))
(declare-fun main_0_tmp_1 () (_ BitVec 32))
(declare-fun arr_val_2 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_2 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_2 () (_ BitVec 32))
(declare-fun arr_next_3 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_0 () (_ BitVec 32))
(declare-fun main_0_temp_i_1 () (_ BitVec 32))
(declare-fun main_0_i_2 () (_ BitVec 32))
(declare-fun main_0_tmp_2 () (_ BitVec 32))
(declare-fun arr_val_3 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_4 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_3 () (_ BitVec 32))
(declare-fun arr_next_5 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_2 () (_ BitVec 32))
(declare-fun main_0_i_3 () (_ BitVec 32))
(declare-fun main_0_tmp_3 () (_ BitVec 32))
(declare-fun arr_val_4 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_6 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_4 () (_ BitVec 32))
(declare-fun arr_next_7 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_3 () (_ BitVec 32))
(declare-fun main_0_i_4 () (_ BitVec 32))
(declare-fun main_0_tmp_4 () (_ BitVec 32))
(declare-fun arr_val_5 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_8 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_5 () (_ BitVec 32))
(declare-fun arr_next_9 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_4 () (_ BitVec 32))
(declare-fun main_0_i_5 () (_ BitVec 32))
(declare-fun main_0_tmp_5 () (_ BitVec 32))
(declare-fun arr_val_6 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_10 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_6 () (_ BitVec 32))
(declare-fun arr_next_11 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_5 () (_ BitVec 32))
(declare-fun main_0_i_6 () (_ BitVec 32))
(declare-fun main_0_tmp_6 () (_ BitVec 32))
(declare-fun arr_val_7 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_12 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_7 () (_ BitVec 32))
(declare-fun arr_next_13 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_6 () (_ BitVec 32))
(declare-fun main_0_i_7 () (_ BitVec 32))
(declare-fun main_0_tmp_7 () (_ BitVec 32))
(declare-fun arr_val_8 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_14 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_8 () (_ BitVec 32))
(declare-fun arr_next_15 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_7 () (_ BitVec 32))
(declare-fun main_0_i_8 () (_ BitVec 32))
(declare-fun main_0_tmp_8 () (_ BitVec 32))
(declare-fun arr_val_9 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_16 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_9 () (_ BitVec 32))
(declare-fun arr_next_17 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_8 () (_ BitVec 32))
(declare-fun main_0_i_9 () (_ BitVec 32))
(declare-fun main_0_tmp_9 () (_ BitVec 32))
(declare-fun arr_val_10 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_18 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_10 () (_ BitVec 32))
(declare-fun arr_next_19 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_9 () (_ BitVec 32))
(declare-fun main_0_i_10 () (_ BitVec 32))
(declare-fun main_0_tmp_10 () (_ BitVec 32))
(declare-fun arr_val_11 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_20 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_11 () (_ BitVec 32))
(declare-fun arr_next_21 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_10 () (_ BitVec 32))
(declare-fun main_0_i_11 () (_ BitVec 32))
(declare-fun main_0_tmp_11 () (_ BitVec 32))
(declare-fun arr_val_12 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_22 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_12 () (_ BitVec 32))
(declare-fun arr_next_23 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_11 () (_ BitVec 32))
(declare-fun main_0_i_12 () (_ BitVec 32))
(declare-fun main_0_tmp_12 () (_ BitVec 32))
(declare-fun arr_val_13 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_24 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_13 () (_ BitVec 32))
(declare-fun arr_next_25 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_12 () (_ BitVec 32))
(declare-fun main_0_i_13 () (_ BitVec 32))
(declare-fun main_0_tmp_13 () (_ BitVec 32))
(declare-fun arr_val_14 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_26 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_14 () (_ BitVec 32))
(declare-fun arr_next_27 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_13 () (_ BitVec 32))
(declare-fun main_0_i_14 () (_ BitVec 32))
(declare-fun main_0_tmp_14 () (_ BitVec 32))
(declare-fun arr_val_15 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_28 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_curr_15 () (_ BitVec 32))
(declare-fun arr_next_29 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_0_temp_i_14 () (_ BitVec 32))
(declare-fun main_0_i_15 () (_ BitVec 32))
(declare-fun undefInt_1 () (_ BitVec 32))
(declare-fun delete_0_val_0 () (_ BitVec 32))
(declare-fun delete_0_val_1 () (_ BitVec 32))
(declare-fun delete_0_list_0 () (_ BitVec 32))
(declare-fun delete_0_list_1 () (_ BitVec 32))
(declare-fun delete_0_head_0 () (_ BitVec 32))
(declare-fun delete_0_head_1 () (_ BitVec 32))
(declare-fun delete_0_head_2 () (_ BitVec 32))
(declare-fun delete_0_head_3 () (_ BitVec 32))
(declare-fun delete_0_head_4 () (_ BitVec 32))
(declare-fun delete_0_head_5 () (_ BitVec 32))
(declare-fun delete_0_head_6 () (_ BitVec 32))
(declare-fun delete_0_head_7 () (_ BitVec 32))
(declare-fun delete_0_head_8 () (_ BitVec 32))
(declare-fun delete_0_head_9 () (_ BitVec 32))
(declare-fun delete_0_head_10 () (_ BitVec 32))
(declare-fun delete_0_head_11 () (_ BitVec 32))
(declare-fun delete_0_head_12 () (_ BitVec 32))
(declare-fun delete_0_head_13 () (_ BitVec 32))
(declare-fun delete_0_head_14 () (_ BitVec 32))
(declare-fun delete_0_head_15 () (_ BitVec 32))
(declare-fun delete_0_prev_0 () (_ BitVec 32))
(declare-fun delete_0_prev_1 () (_ BitVec 32))
(declare-fun delete_0_curr_0 () (_ BitVec 32))
(declare-fun delete_0_curr_1 () (_ BitVec 32))
(declare-fun arr_next_30 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_2 () (_ BitVec 32))
(declare-fun delete_0_prev_2 () (_ BitVec 32))
(declare-fun delete_0_curr_3 () (_ BitVec 32))
(declare-fun arr_next_31 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_4 () (_ BitVec 32))
(declare-fun delete_0_prev_3 () (_ BitVec 32))
(declare-fun delete_0_curr_5 () (_ BitVec 32))
(declare-fun arr_next_32 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_6 () (_ BitVec 32))
(declare-fun delete_0_prev_4 () (_ BitVec 32))
(declare-fun delete_0_curr_7 () (_ BitVec 32))
(declare-fun arr_next_33 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_8 () (_ BitVec 32))
(declare-fun delete_0_prev_5 () (_ BitVec 32))
(declare-fun delete_0_curr_9 () (_ BitVec 32))
(declare-fun arr_next_34 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_10 () (_ BitVec 32))
(declare-fun delete_0_prev_6 () (_ BitVec 32))
(declare-fun delete_0_curr_11 () (_ BitVec 32))
(declare-fun arr_next_35 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_12 () (_ BitVec 32))
(declare-fun delete_0_prev_7 () (_ BitVec 32))
(declare-fun delete_0_curr_13 () (_ BitVec 32))
(declare-fun arr_next_36 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_14 () (_ BitVec 32))
(declare-fun delete_0_prev_8 () (_ BitVec 32))
(declare-fun delete_0_curr_15 () (_ BitVec 32))
(declare-fun arr_next_37 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_16 () (_ BitVec 32))
(declare-fun delete_0_prev_9 () (_ BitVec 32))
(declare-fun delete_0_curr_17 () (_ BitVec 32))
(declare-fun arr_next_38 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_18 () (_ BitVec 32))
(declare-fun delete_0_prev_10 () (_ BitVec 32))
(declare-fun delete_0_curr_19 () (_ BitVec 32))
(declare-fun arr_next_39 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_20 () (_ BitVec 32))
(declare-fun delete_0_prev_11 () (_ BitVec 32))
(declare-fun delete_0_curr_21 () (_ BitVec 32))
(declare-fun arr_next_40 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_22 () (_ BitVec 32))
(declare-fun delete_0_prev_12 () (_ BitVec 32))
(declare-fun delete_0_curr_23 () (_ BitVec 32))
(declare-fun arr_next_41 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_24 () (_ BitVec 32))
(declare-fun delete_0_prev_13 () (_ BitVec 32))
(declare-fun delete_0_curr_25 () (_ BitVec 32))
(declare-fun arr_next_42 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_26 () (_ BitVec 32))
(declare-fun delete_0_prev_14 () (_ BitVec 32))
(declare-fun delete_0_curr_27 () (_ BitVec 32))
(declare-fun arr_next_43 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun delete_0_curr_28 () (_ BitVec 32))
(declare-fun delete_0_prev_15 () (_ BitVec 32))
(declare-fun delete_0_curr_29 () (_ BitVec 32))
(declare-fun delete_return_0 () (_ BitVec 32))
(declare-fun delete_return_1 () (_ BitVec 32))
(declare-fun main_0_head_2 () (_ BitVec 32))
(declare-fun main_0_x_0 () (_ BitVec 32))
(declare-fun member_0_val_0 () (_ BitVec 32))
(declare-fun member_0_val_1 () (_ BitVec 32))
(declare-fun member_0_head_0 () (_ BitVec 32))
(declare-fun member_0_head_1 () (_ BitVec 32))
(declare-fun member_0_curr_0 () (_ BitVec 32))
(declare-fun member_0_curr_1 () (_ BitVec 32))
(declare-fun member_0_result_0 () (_ BitVec 32))
(declare-fun member_0_result_1 () (_ BitVec 32))
(declare-fun member_0_curr_2 () (_ BitVec 32))
(declare-fun member_0_result_2 () (_ BitVec 32))
(declare-fun member_0_curr_3 () (_ BitVec 32))
(declare-fun member_0_result_3 () (_ BitVec 32))
(declare-fun member_0_curr_4 () (_ BitVec 32))
(declare-fun member_0_result_4 () (_ BitVec 32))
(declare-fun member_0_curr_5 () (_ BitVec 32))
(declare-fun member_0_result_5 () (_ BitVec 32))
(declare-fun member_0_curr_6 () (_ BitVec 32))
(declare-fun member_0_result_6 () (_ BitVec 32))
(declare-fun member_0_curr_7 () (_ BitVec 32))
(declare-fun member_0_result_7 () (_ BitVec 32))
(declare-fun member_0_curr_8 () (_ BitVec 32))
(declare-fun member_0_result_8 () (_ BitVec 32))
(declare-fun member_0_curr_9 () (_ BitVec 32))
(declare-fun member_0_result_9 () (_ BitVec 32))
(declare-fun member_0_curr_10 () (_ BitVec 32))
(declare-fun member_0_result_10 () (_ BitVec 32))
(declare-fun member_0_curr_11 () (_ BitVec 32))
(declare-fun member_0_result_11 () (_ BitVec 32))
(declare-fun member_0_curr_12 () (_ BitVec 32))
(declare-fun member_0_result_12 () (_ BitVec 32))
(declare-fun member_0_curr_13 () (_ BitVec 32))
(declare-fun member_0_result_13 () (_ BitVec 32))
(declare-fun member_0_curr_14 () (_ BitVec 32))
(declare-fun member_0_result_14 () (_ BitVec 32))
(declare-fun member_0_curr_15 () (_ BitVec 32))
(declare-fun member_0_result_15 () (_ BitVec 32))
(declare-fun main_0_x_1 () (_ BitVec 32))
(assert (= main_0_head_1 (_ bv0 32)))
(assert (= arr_val_1 (store arr_val_0 main_0_head_1 (_ bv0 32))))
(assert (= arr_next_1 (store arr_next_0 main_0_head_1 (bvneg (_ bv1 32)))))
(assert (= main_0_curr_1 main_0_head_1))
(assert (= main_0_i_1 (_ bv1 32)))
(assert (= main_0_tmp_1 (ite (bvult main_0_i_1 (_ bv13 32)) (_ bv1 32) main_0_tmp_0)))
(assert (= arr_val_2 (ite (bvult main_0_i_1 (_ bv13 32)) (store arr_val_1 main_0_tmp_1 main_0_i_1) arr_val_1)))
(assert (= arr_next_2 (ite (bvult main_0_i_1 (_ bv13 32)) (store arr_next_1 main_0_curr_1 main_0_tmp_1) arr_next_1)))
(assert (= main_0_curr_2 (ite (bvult main_0_i_1 (_ bv13 32)) (select arr_next_2 main_0_curr_1) main_0_curr_1)))
(assert (= arr_next_3 (ite (bvult main_0_i_1 (_ bv13 32)) (store arr_next_2 main_0_tmp_1 (bvneg (_ bv1 32))) arr_next_2)))
(assert (= main_0_temp_i_1 (ite (bvult main_0_i_1 (_ bv13 32)) main_0_i_1 main_0_temp_i_0)))
(assert (= main_0_i_2 (ite (bvult main_0_i_1 (_ bv13 32)) (bvadd main_0_i_1 (_ bv1 32)) main_0_i_1)))
(assert (= main_0_tmp_2 (ite (bvult main_0_i_2 (_ bv13 32)) (_ bv2 32) main_0_tmp_1)))
(assert (= arr_val_3 (ite (bvult main_0_i_2 (_ bv13 32)) (store arr_val_2 main_0_tmp_2 main_0_i_2) arr_val_2)))
(assert (= arr_next_4 (ite (bvult main_0_i_2 (_ bv13 32)) (store arr_next_3 main_0_curr_2 main_0_tmp_2) arr_next_3)))
(assert (= main_0_curr_3 (ite (bvult main_0_i_2 (_ bv13 32)) (select arr_next_4 main_0_curr_2) main_0_curr_2)))
(assert (= arr_next_5 (ite (bvult main_0_i_2 (_ bv13 32)) (store arr_next_4 main_0_tmp_2 (bvneg (_ bv1 32))) arr_next_4)))
(assert (= main_0_temp_i_2 (ite (bvult main_0_i_2 (_ bv13 32)) main_0_i_2 main_0_temp_i_1)))
(assert (= main_0_i_3 (ite (bvult main_0_i_2 (_ bv13 32)) (bvadd main_0_i_2 (_ bv1 32)) main_0_i_2)))
(assert (= main_0_tmp_3 (ite (bvult main_0_i_3 (_ bv13 32)) (_ bv3 32) main_0_tmp_2)))
(assert (= arr_val_4 (ite (bvult main_0_i_3 (_ bv13 32)) (store arr_val_3 main_0_tmp_3 main_0_i_3) arr_val_3)))
(assert (= arr_next_6 (ite (bvult main_0_i_3 (_ bv13 32)) (store arr_next_5 main_0_curr_3 main_0_tmp_3) arr_next_5)))
(assert (= main_0_curr_4 (ite (bvult main_0_i_3 (_ bv13 32)) (select arr_next_6 main_0_curr_3) main_0_curr_3)))
(assert (= arr_next_7 (ite (bvult main_0_i_3 (_ bv13 32)) (store arr_next_6 main_0_tmp_3 (bvneg (_ bv1 32))) arr_next_6)))
(assert (= main_0_temp_i_3 (ite (bvult main_0_i_3 (_ bv13 32)) main_0_i_3 main_0_temp_i_2)))
(assert (= main_0_i_4 (ite (bvult main_0_i_3 (_ bv13 32)) (bvadd main_0_i_3 (_ bv1 32)) main_0_i_3)))
(assert (= main_0_tmp_4 (ite (bvult main_0_i_4 (_ bv13 32)) (_ bv4 32) main_0_tmp_3)))
(assert (= arr_val_5 (ite (bvult main_0_i_4 (_ bv13 32)) (store arr_val_4 main_0_tmp_4 main_0_i_4) arr_val_4)))
(assert (= arr_next_8 (ite (bvult main_0_i_4 (_ bv13 32)) (store arr_next_7 main_0_curr_4 main_0_tmp_4) arr_next_7)))
(assert (= main_0_curr_5 (ite (bvult main_0_i_4 (_ bv13 32)) (select arr_next_8 main_0_curr_4) main_0_curr_4)))
(assert (= arr_next_9 (ite (bvult main_0_i_4 (_ bv13 32)) (store arr_next_8 main_0_tmp_4 (bvneg (_ bv1 32))) arr_next_8)))
(assert (= main_0_temp_i_4 (ite (bvult main_0_i_4 (_ bv13 32)) main_0_i_4 main_0_temp_i_3)))
(assert (= main_0_i_5 (ite (bvult main_0_i_4 (_ bv13 32)) (bvadd main_0_i_4 (_ bv1 32)) main_0_i_4)))
(assert (= main_0_tmp_5 (ite (bvult main_0_i_5 (_ bv13 32)) (_ bv5 32) main_0_tmp_4)))
(assert (= arr_val_6 (ite (bvult main_0_i_5 (_ bv13 32)) (store arr_val_5 main_0_tmp_5 main_0_i_5) arr_val_5)))
(assert (= arr_next_10 (ite (bvult main_0_i_5 (_ bv13 32)) (store arr_next_9 main_0_curr_5 main_0_tmp_5) arr_next_9)))
(assert (= main_0_curr_6 (ite (bvult main_0_i_5 (_ bv13 32)) (select arr_next_10 main_0_curr_5) main_0_curr_5)))
(assert (= arr_next_11 (ite (bvult main_0_i_5 (_ bv13 32)) (store arr_next_10 main_0_tmp_5 (bvneg (_ bv1 32))) arr_next_10)))
(assert (= main_0_temp_i_5 (ite (bvult main_0_i_5 (_ bv13 32)) main_0_i_5 main_0_temp_i_4)))
(assert (= main_0_i_6 (ite (bvult main_0_i_5 (_ bv13 32)) (bvadd main_0_i_5 (_ bv1 32)) main_0_i_5)))
(assert (= main_0_tmp_6 (ite (bvult main_0_i_6 (_ bv13 32)) (_ bv6 32) main_0_tmp_5)))
(assert (= arr_val_7 (ite (bvult main_0_i_6 (_ bv13 32)) (store arr_val_6 main_0_tmp_6 main_0_i_6) arr_val_6)))
(assert (= arr_next_12 (ite (bvult main_0_i_6 (_ bv13 32)) (store arr_next_11 main_0_curr_6 main_0_tmp_6) arr_next_11)))
(assert (= main_0_curr_7 (ite (bvult main_0_i_6 (_ bv13 32)) (select arr_next_12 main_0_curr_6) main_0_curr_6)))
(assert (= arr_next_13 (ite (bvult main_0_i_6 (_ bv13 32)) (store arr_next_12 main_0_tmp_6 (bvneg (_ bv1 32))) arr_next_12)))
(assert (= main_0_temp_i_6 (ite (bvult main_0_i_6 (_ bv13 32)) main_0_i_6 main_0_temp_i_5)))
(assert (= main_0_i_7 (ite (bvult main_0_i_6 (_ bv13 32)) (bvadd main_0_i_6 (_ bv1 32)) main_0_i_6)))
(assert (= main_0_tmp_7 (ite (bvult main_0_i_7 (_ bv13 32)) (_ bv7 32) main_0_tmp_6)))
(assert (= arr_val_8 (ite (bvult main_0_i_7 (_ bv13 32)) (store arr_val_7 main_0_tmp_7 main_0_i_7) arr_val_7)))
(assert (= arr_next_14 (ite (bvult main_0_i_7 (_ bv13 32)) (store arr_next_13 main_0_curr_7 main_0_tmp_7) arr_next_13)))
(assert (= main_0_curr_8 (ite (bvult main_0_i_7 (_ bv13 32)) (select arr_next_14 main_0_curr_7) main_0_curr_7)))
(assert (= arr_next_15 (ite (bvult main_0_i_7 (_ bv13 32)) (store arr_next_14 main_0_tmp_7 (bvneg (_ bv1 32))) arr_next_14)))
(assert (= main_0_temp_i_7 (ite (bvult main_0_i_7 (_ bv13 32)) main_0_i_7 main_0_temp_i_6)))
(assert (= main_0_i_8 (ite (bvult main_0_i_7 (_ bv13 32)) (bvadd main_0_i_7 (_ bv1 32)) main_0_i_7)))
(assert (= main_0_tmp_8 (ite (bvult main_0_i_8 (_ bv13 32)) (_ bv8 32) main_0_tmp_7)))
(assert (= arr_val_9 (ite (bvult main_0_i_8 (_ bv13 32)) (store arr_val_8 main_0_tmp_8 main_0_i_8) arr_val_8)))
(assert (= arr_next_16 (ite (bvult main_0_i_8 (_ bv13 32)) (store arr_next_15 main_0_curr_8 main_0_tmp_8) arr_next_15)))
(assert (= main_0_curr_9 (ite (bvult main_0_i_8 (_ bv13 32)) (select arr_next_16 main_0_curr_8) main_0_curr_8)))
(assert (= arr_next_17 (ite (bvult main_0_i_8 (_ bv13 32)) (store arr_next_16 main_0_tmp_8 (bvneg (_ bv1 32))) arr_next_16)))
(assert (= main_0_temp_i_8 (ite (bvult main_0_i_8 (_ bv13 32)) main_0_i_8 main_0_temp_i_7)))
(assert (= main_0_i_9 (ite (bvult main_0_i_8 (_ bv13 32)) (bvadd main_0_i_8 (_ bv1 32)) main_0_i_8)))
(assert (= main_0_tmp_9 (ite (bvult main_0_i_9 (_ bv13 32)) (_ bv9 32) main_0_tmp_8)))
(assert (= arr_val_10 (ite (bvult main_0_i_9 (_ bv13 32)) (store arr_val_9 main_0_tmp_9 main_0_i_9) arr_val_9)))
(assert (= arr_next_18 (ite (bvult main_0_i_9 (_ bv13 32)) (store arr_next_17 main_0_curr_9 main_0_tmp_9) arr_next_17)))
(assert (= main_0_curr_10 (ite (bvult main_0_i_9 (_ bv13 32)) (select arr_next_18 main_0_curr_9) main_0_curr_9)))
(assert (= arr_next_19 (ite (bvult main_0_i_9 (_ bv13 32)) (store arr_next_18 main_0_tmp_9 (bvneg (_ bv1 32))) arr_next_18)))
(assert (= main_0_temp_i_9 (ite (bvult main_0_i_9 (_ bv13 32)) main_0_i_9 main_0_temp_i_8)))
(assert (= main_0_i_10 (ite (bvult main_0_i_9 (_ bv13 32)) (bvadd main_0_i_9 (_ bv1 32)) main_0_i_9)))
(assert (= main_0_tmp_10 (ite (bvult main_0_i_10 (_ bv13 32)) (_ bv10 32) main_0_tmp_9)))
(assert (= arr_val_11 (ite (bvult main_0_i_10 (_ bv13 32)) (store arr_val_10 main_0_tmp_10 main_0_i_10) arr_val_10)))
(assert (= arr_next_20 (ite (bvult main_0_i_10 (_ bv13 32)) (store arr_next_19 main_0_curr_10 main_0_tmp_10) arr_next_19)))
(assert (= main_0_curr_11 (ite (bvult main_0_i_10 (_ bv13 32)) (select arr_next_20 main_0_curr_10) main_0_curr_10)))
(assert (= arr_next_21 (ite (bvult main_0_i_10 (_ bv13 32)) (store arr_next_20 main_0_tmp_10 (bvneg (_ bv1 32))) arr_next_20)))
(assert (= main_0_temp_i_10 (ite (bvult main_0_i_10 (_ bv13 32)) main_0_i_10 main_0_temp_i_9)))
(assert (= main_0_i_11 (ite (bvult main_0_i_10 (_ bv13 32)) (bvadd main_0_i_10 (_ bv1 32)) main_0_i_10)))
(assert (= main_0_tmp_11 (ite (bvult main_0_i_11 (_ bv13 32)) (_ bv11 32) main_0_tmp_10)))
(assert (= arr_val_12 (ite (bvult main_0_i_11 (_ bv13 32)) (store arr_val_11 main_0_tmp_11 main_0_i_11) arr_val_11)))
(assert (= arr_next_22 (ite (bvult main_0_i_11 (_ bv13 32)) (store arr_next_21 main_0_curr_11 main_0_tmp_11) arr_next_21)))
(assert (= main_0_curr_12 (ite (bvult main_0_i_11 (_ bv13 32)) (select arr_next_22 main_0_curr_11) main_0_curr_11)))
(assert (= arr_next_23 (ite (bvult main_0_i_11 (_ bv13 32)) (store arr_next_22 main_0_tmp_11 (bvneg (_ bv1 32))) arr_next_22)))
(assert (= main_0_temp_i_11 (ite (bvult main_0_i_11 (_ bv13 32)) main_0_i_11 main_0_temp_i_10)))
(assert (= main_0_i_12 (ite (bvult main_0_i_11 (_ bv13 32)) (bvadd main_0_i_11 (_ bv1 32)) main_0_i_11)))
(assert (= main_0_tmp_12 (ite (bvult main_0_i_12 (_ bv13 32)) (_ bv12 32) main_0_tmp_11)))
(assert (= arr_val_13 (ite (bvult main_0_i_12 (_ bv13 32)) (store arr_val_12 main_0_tmp_12 main_0_i_12) arr_val_12)))
(assert (= arr_next_24 (ite (bvult main_0_i_12 (_ bv13 32)) (store arr_next_23 main_0_curr_12 main_0_tmp_12) arr_next_23)))
(assert (= main_0_curr_13 (ite (bvult main_0_i_12 (_ bv13 32)) (select arr_next_24 main_0_curr_12) main_0_curr_12)))
(assert (= arr_next_25 (ite (bvult main_0_i_12 (_ bv13 32)) (store arr_next_24 main_0_tmp_12 (bvneg (_ bv1 32))) arr_next_24)))
(assert (= main_0_temp_i_12 (ite (bvult main_0_i_12 (_ bv13 32)) main_0_i_12 main_0_temp_i_11)))
(assert (= main_0_i_13 (ite (bvult main_0_i_12 (_ bv13 32)) (bvadd main_0_i_12 (_ bv1 32)) main_0_i_12)))
(assert (= main_0_tmp_13 (ite (bvult main_0_i_13 (_ bv13 32)) (_ bv13 32) main_0_tmp_12)))
(assert (= arr_val_14 (ite (bvult main_0_i_13 (_ bv13 32)) (store arr_val_13 main_0_tmp_13 main_0_i_13) arr_val_13)))
(assert (= arr_next_26 (ite (bvult main_0_i_13 (_ bv13 32)) (store arr_next_25 main_0_curr_13 main_0_tmp_13) arr_next_25)))
(assert (= main_0_curr_14 (ite (bvult main_0_i_13 (_ bv13 32)) (select arr_next_26 main_0_curr_13) main_0_curr_13)))
(assert (= arr_next_27 (ite (bvult main_0_i_13 (_ bv13 32)) (store arr_next_26 main_0_tmp_13 (bvneg (_ bv1 32))) arr_next_26)))
(assert (= main_0_temp_i_13 (ite (bvult main_0_i_13 (_ bv13 32)) main_0_i_13 main_0_temp_i_12)))
(assert (= main_0_i_14 (ite (bvult main_0_i_13 (_ bv13 32)) (bvadd main_0_i_13 (_ bv1 32)) main_0_i_13)))
(assert (= main_0_tmp_14 (ite (bvult main_0_i_14 (_ bv13 32)) (_ bv14 32) main_0_tmp_13)))
(assert (= arr_val_15 (ite (bvult main_0_i_14 (_ bv13 32)) (store arr_val_14 main_0_tmp_14 main_0_i_14) arr_val_14)))
(assert (= arr_next_28 (ite (bvult main_0_i_14 (_ bv13 32)) (store arr_next_27 main_0_curr_14 main_0_tmp_14) arr_next_27)))
(assert (= main_0_curr_15 (ite (bvult main_0_i_14 (_ bv13 32)) (select arr_next_28 main_0_curr_14) main_0_curr_14)))
(assert (= arr_next_29 (ite (bvult main_0_i_14 (_ bv13 32)) (store arr_next_28 main_0_tmp_14 (bvneg (_ bv1 32))) arr_next_28)))
(assert (= main_0_temp_i_14 (ite (bvult main_0_i_14 (_ bv13 32)) main_0_i_14 main_0_temp_i_13)))
(assert (= main_0_i_15 (ite (bvult main_0_i_14 (_ bv13 32)) (bvadd main_0_i_14 (_ bv1 32)) main_0_i_14)))
(assert (= delete_0_val_1 undefInt_1))
(assert (= delete_0_list_1 main_0_head_1))
(assert (= delete_0_head_1 delete_0_list_1))
(assert (let ((_let_0 (select arr_next_29 delete_0_head_1))) (= delete_0_head_2 (ite (and (= (select arr_val_15 delete_0_head_1) delete_0_val_1) (not (= _let_0 (bvneg (_ bv1 32))))) _let_0 delete_0_head_1))))
(assert (= delete_0_head_3 (ite (and (= (select arr_val_15 delete_0_head_2) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_2) delete_0_head_2)))
(assert (= delete_0_head_4 (ite (and (= (select arr_val_15 delete_0_head_3) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_3) delete_0_head_3)))
(assert (= delete_0_head_5 (ite (and (= (select arr_val_15 delete_0_head_4) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_4) delete_0_head_4)))
(assert (= delete_0_head_6 (ite (and (= (select arr_val_15 delete_0_head_5) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_5) delete_0_head_5)))
(assert (= delete_0_head_7 (ite (and (= (select arr_val_15 delete_0_head_6) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_6) delete_0_head_6)))
(assert (= delete_0_head_8 (ite (and (= (select arr_val_15 delete_0_head_7) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_7) delete_0_head_7)))
(assert (= delete_0_head_9 (ite (and (= (select arr_val_15 delete_0_head_8) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_8) delete_0_head_8)))
(assert (= delete_0_head_10 (ite (and (= (select arr_val_15 delete_0_head_9) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_9) delete_0_head_9)))
(assert (= delete_0_head_11 (ite (and (= (select arr_val_15 delete_0_head_10) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_10) delete_0_head_10)))
(assert (= delete_0_head_12 (ite (and (= (select arr_val_15 delete_0_head_11) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_11) delete_0_head_11)))
(assert (= delete_0_head_13 (ite (and (= (select arr_val_15 delete_0_head_12) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_12) delete_0_head_12)))
(assert (= delete_0_head_14 (ite (and (= (select arr_val_15 delete_0_head_13) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_13) delete_0_head_13)))
(assert (= delete_0_head_15 (ite (and (= (select arr_val_15 delete_0_head_14) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32))))) (select arr_next_29 delete_0_head_14) delete_0_head_14)))
(assert (= delete_0_prev_1 (ite (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32)))) delete_0_head_15 delete_0_prev_0)))
(assert (= delete_0_curr_1 (ite (not (= (select arr_next_29 delete_0_head_1) (bvneg (_ bv1 32)))) (select arr_next_29 delete_0_head_15) delete_0_curr_0)))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_30 (ite (and (and (not (= delete_0_curr_1 _let_0)) (= (select arr_val_15 delete_0_curr_1) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_29 delete_0_prev_1 (select arr_next_29 delete_0_curr_1)) arr_next_29))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_2 (ite (and (and (not (= delete_0_curr_1 _let_0)) (= (select arr_val_15 delete_0_curr_1) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_30 delete_0_curr_1) delete_0_curr_1))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_2 (ite (and (and (not (= delete_0_curr_1 _let_0)) (not (= (select arr_val_15 delete_0_curr_1) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_2 delete_0_prev_1))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_3 (ite (and (and (not (= delete_0_curr_1 _let_0)) (not (= (select arr_val_15 delete_0_curr_1) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_30 delete_0_curr_2) delete_0_curr_2))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_31 (ite (and (and (not (= delete_0_curr_3 _let_0)) (= (select arr_val_15 delete_0_curr_3) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_30 delete_0_prev_2 (select arr_next_30 delete_0_curr_3)) arr_next_30))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_4 (ite (and (and (not (= delete_0_curr_3 _let_0)) (= (select arr_val_15 delete_0_curr_3) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_31 delete_0_curr_3) delete_0_curr_3))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_3 (ite (and (and (not (= delete_0_curr_3 _let_0)) (not (= (select arr_val_15 delete_0_curr_3) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_4 delete_0_prev_2))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_5 (ite (and (and (not (= delete_0_curr_3 _let_0)) (not (= (select arr_val_15 delete_0_curr_3) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_31 delete_0_curr_4) delete_0_curr_4))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_32 (ite (and (and (not (= delete_0_curr_5 _let_0)) (= (select arr_val_15 delete_0_curr_5) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_31 delete_0_prev_3 (select arr_next_31 delete_0_curr_5)) arr_next_31))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_6 (ite (and (and (not (= delete_0_curr_5 _let_0)) (= (select arr_val_15 delete_0_curr_5) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_32 delete_0_curr_5) delete_0_curr_5))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_4 (ite (and (and (not (= delete_0_curr_5 _let_0)) (not (= (select arr_val_15 delete_0_curr_5) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_6 delete_0_prev_3))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_7 (ite (and (and (not (= delete_0_curr_5 _let_0)) (not (= (select arr_val_15 delete_0_curr_5) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_32 delete_0_curr_6) delete_0_curr_6))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_33 (ite (and (and (not (= delete_0_curr_7 _let_0)) (= (select arr_val_15 delete_0_curr_7) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_32 delete_0_prev_4 (select arr_next_32 delete_0_curr_7)) arr_next_32))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_8 (ite (and (and (not (= delete_0_curr_7 _let_0)) (= (select arr_val_15 delete_0_curr_7) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_33 delete_0_curr_7) delete_0_curr_7))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_5 (ite (and (and (not (= delete_0_curr_7 _let_0)) (not (= (select arr_val_15 delete_0_curr_7) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_8 delete_0_prev_4))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_9 (ite (and (and (not (= delete_0_curr_7 _let_0)) (not (= (select arr_val_15 delete_0_curr_7) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_33 delete_0_curr_8) delete_0_curr_8))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_34 (ite (and (and (not (= delete_0_curr_9 _let_0)) (= (select arr_val_15 delete_0_curr_9) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_33 delete_0_prev_5 (select arr_next_33 delete_0_curr_9)) arr_next_33))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_10 (ite (and (and (not (= delete_0_curr_9 _let_0)) (= (select arr_val_15 delete_0_curr_9) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_34 delete_0_curr_9) delete_0_curr_9))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_6 (ite (and (and (not (= delete_0_curr_9 _let_0)) (not (= (select arr_val_15 delete_0_curr_9) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_10 delete_0_prev_5))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_11 (ite (and (and (not (= delete_0_curr_9 _let_0)) (not (= (select arr_val_15 delete_0_curr_9) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_34 delete_0_curr_10) delete_0_curr_10))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_35 (ite (and (and (not (= delete_0_curr_11 _let_0)) (= (select arr_val_15 delete_0_curr_11) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_34 delete_0_prev_6 (select arr_next_34 delete_0_curr_11)) arr_next_34))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_12 (ite (and (and (not (= delete_0_curr_11 _let_0)) (= (select arr_val_15 delete_0_curr_11) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_35 delete_0_curr_11) delete_0_curr_11))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_7 (ite (and (and (not (= delete_0_curr_11 _let_0)) (not (= (select arr_val_15 delete_0_curr_11) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_12 delete_0_prev_6))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_13 (ite (and (and (not (= delete_0_curr_11 _let_0)) (not (= (select arr_val_15 delete_0_curr_11) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_35 delete_0_curr_12) delete_0_curr_12))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_36 (ite (and (and (not (= delete_0_curr_13 _let_0)) (= (select arr_val_15 delete_0_curr_13) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_35 delete_0_prev_7 (select arr_next_35 delete_0_curr_13)) arr_next_35))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_14 (ite (and (and (not (= delete_0_curr_13 _let_0)) (= (select arr_val_15 delete_0_curr_13) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_36 delete_0_curr_13) delete_0_curr_13))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_8 (ite (and (and (not (= delete_0_curr_13 _let_0)) (not (= (select arr_val_15 delete_0_curr_13) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_14 delete_0_prev_7))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_15 (ite (and (and (not (= delete_0_curr_13 _let_0)) (not (= (select arr_val_15 delete_0_curr_13) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_36 delete_0_curr_14) delete_0_curr_14))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_37 (ite (and (and (not (= delete_0_curr_15 _let_0)) (= (select arr_val_15 delete_0_curr_15) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_36 delete_0_prev_8 (select arr_next_36 delete_0_curr_15)) arr_next_36))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_16 (ite (and (and (not (= delete_0_curr_15 _let_0)) (= (select arr_val_15 delete_0_curr_15) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_37 delete_0_curr_15) delete_0_curr_15))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_9 (ite (and (and (not (= delete_0_curr_15 _let_0)) (not (= (select arr_val_15 delete_0_curr_15) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_16 delete_0_prev_8))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_17 (ite (and (and (not (= delete_0_curr_15 _let_0)) (not (= (select arr_val_15 delete_0_curr_15) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_37 delete_0_curr_16) delete_0_curr_16))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_38 (ite (and (and (not (= delete_0_curr_17 _let_0)) (= (select arr_val_15 delete_0_curr_17) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_37 delete_0_prev_9 (select arr_next_37 delete_0_curr_17)) arr_next_37))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_18 (ite (and (and (not (= delete_0_curr_17 _let_0)) (= (select arr_val_15 delete_0_curr_17) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_38 delete_0_curr_17) delete_0_curr_17))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_10 (ite (and (and (not (= delete_0_curr_17 _let_0)) (not (= (select arr_val_15 delete_0_curr_17) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_18 delete_0_prev_9))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_19 (ite (and (and (not (= delete_0_curr_17 _let_0)) (not (= (select arr_val_15 delete_0_curr_17) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_38 delete_0_curr_18) delete_0_curr_18))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_39 (ite (and (and (not (= delete_0_curr_19 _let_0)) (= (select arr_val_15 delete_0_curr_19) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_38 delete_0_prev_10 (select arr_next_38 delete_0_curr_19)) arr_next_38))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_20 (ite (and (and (not (= delete_0_curr_19 _let_0)) (= (select arr_val_15 delete_0_curr_19) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_39 delete_0_curr_19) delete_0_curr_19))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_11 (ite (and (and (not (= delete_0_curr_19 _let_0)) (not (= (select arr_val_15 delete_0_curr_19) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_20 delete_0_prev_10))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_21 (ite (and (and (not (= delete_0_curr_19 _let_0)) (not (= (select arr_val_15 delete_0_curr_19) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_39 delete_0_curr_20) delete_0_curr_20))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_40 (ite (and (and (not (= delete_0_curr_21 _let_0)) (= (select arr_val_15 delete_0_curr_21) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_39 delete_0_prev_11 (select arr_next_39 delete_0_curr_21)) arr_next_39))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_22 (ite (and (and (not (= delete_0_curr_21 _let_0)) (= (select arr_val_15 delete_0_curr_21) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_40 delete_0_curr_21) delete_0_curr_21))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_12 (ite (and (and (not (= delete_0_curr_21 _let_0)) (not (= (select arr_val_15 delete_0_curr_21) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_22 delete_0_prev_11))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_23 (ite (and (and (not (= delete_0_curr_21 _let_0)) (not (= (select arr_val_15 delete_0_curr_21) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_40 delete_0_curr_22) delete_0_curr_22))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_41 (ite (and (and (not (= delete_0_curr_23 _let_0)) (= (select arr_val_15 delete_0_curr_23) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_40 delete_0_prev_12 (select arr_next_40 delete_0_curr_23)) arr_next_40))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_24 (ite (and (and (not (= delete_0_curr_23 _let_0)) (= (select arr_val_15 delete_0_curr_23) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_41 delete_0_curr_23) delete_0_curr_23))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_13 (ite (and (and (not (= delete_0_curr_23 _let_0)) (not (= (select arr_val_15 delete_0_curr_23) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_24 delete_0_prev_12))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_25 (ite (and (and (not (= delete_0_curr_23 _let_0)) (not (= (select arr_val_15 delete_0_curr_23) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_41 delete_0_curr_24) delete_0_curr_24))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_42 (ite (and (and (not (= delete_0_curr_25 _let_0)) (= (select arr_val_15 delete_0_curr_25) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_41 delete_0_prev_13 (select arr_next_41 delete_0_curr_25)) arr_next_41))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_26 (ite (and (and (not (= delete_0_curr_25 _let_0)) (= (select arr_val_15 delete_0_curr_25) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_42 delete_0_curr_25) delete_0_curr_25))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_14 (ite (and (and (not (= delete_0_curr_25 _let_0)) (not (= (select arr_val_15 delete_0_curr_25) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_26 delete_0_prev_13))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_27 (ite (and (and (not (= delete_0_curr_25 _let_0)) (not (= (select arr_val_15 delete_0_curr_25) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_42 delete_0_curr_26) delete_0_curr_26))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= arr_next_43 (ite (and (and (not (= delete_0_curr_27 _let_0)) (= (select arr_val_15 delete_0_curr_27) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (store arr_next_42 delete_0_prev_14 (select arr_next_42 delete_0_curr_27)) arr_next_42))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_28 (ite (and (and (not (= delete_0_curr_27 _let_0)) (= (select arr_val_15 delete_0_curr_27) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_43 delete_0_curr_27) delete_0_curr_27))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_prev_15 (ite (and (and (not (= delete_0_curr_27 _let_0)) (not (= (select arr_val_15 delete_0_curr_27) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) delete_0_curr_28 delete_0_prev_14))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= delete_0_curr_29 (ite (and (and (not (= delete_0_curr_27 _let_0)) (not (= (select arr_val_15 delete_0_curr_27) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) _let_0))) (select arr_next_43 delete_0_curr_28) delete_0_curr_28))))
(assert (= delete_return_1 delete_0_head_15))
(assert (= main_0_head_2 delete_return_1))
(assert (= member_0_val_1 (_ bv0 32)))
(assert (= member_0_head_1 main_0_head_2))
(assert (= member_0_curr_1 member_0_head_1))
(assert (= member_0_result_1 (ite (and (not (= member_0_curr_1 (bvneg (_ bv1 32)))) (= (select arr_val_15 member_0_curr_1) member_0_val_1)) (_ bv1 32) member_0_result_0)))
(assert (let ((_let_0 (not (= member_0_curr_1 (bvneg (_ bv1 32)))))) (= member_0_curr_2 (ite (and (not (and _let_0 (= (select arr_val_15 member_0_curr_1) member_0_val_1))) _let_0) (select arr_next_43 member_0_curr_1) member_0_curr_1))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_2 (ite (and (and (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1))) (not (= member_0_curr_2 _let_0))) (= (select arr_val_15 member_0_curr_2) member_0_val_1)) (_ bv1 32) member_0_result_1))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_2 _let_0)))) (= member_0_curr_3 (ite (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_2) member_0_val_1))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_2) member_0_curr_2)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_3 (ite (and (and (and (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_3 _let_0))) (= (select arr_val_15 member_0_curr_3) member_0_val_1)) (_ bv1 32) member_0_result_2))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_3 _let_0)))) (= member_0_curr_4 (ite (and (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_3) member_0_val_1))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_3) member_0_curr_3)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_4 (ite (and (and (and (and (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_4 _let_0))) (= (select arr_val_15 member_0_curr_4) member_0_val_1)) (_ bv1 32) member_0_result_3))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_4 _let_0)))) (= member_0_curr_5 (ite (and (and (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_4) member_0_val_1))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_4) member_0_curr_4)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_5 (ite (and (and (and (and (and (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_5 _let_0))) (= (select arr_val_15 member_0_curr_5) member_0_val_1)) (_ bv1 32) member_0_result_4))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_5 _let_0)))) (= member_0_curr_6 (ite (and (and (and (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_5) member_0_val_1))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_5) member_0_curr_5)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_6 (ite (and (and (and (and (and (and (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_6 _let_0))) (= (select arr_val_15 member_0_curr_6) member_0_val_1)) (_ bv1 32) member_0_result_5))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_6 _let_0)))) (= member_0_curr_7 (ite (and (and (and (and (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_6) member_0_val_1))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_6) member_0_curr_6)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_7 (ite (and (and (and (and (and (and (and (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_7 _let_0))) (= (select arr_val_15 member_0_curr_7) member_0_val_1)) (_ bv1 32) member_0_result_6))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_7 _let_0)))) (= member_0_curr_8 (ite (and (and (and (and (and (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_7) member_0_val_1))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_7) member_0_curr_7)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_8 (ite (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_8 _let_0))) (= (select arr_val_15 member_0_curr_8) member_0_val_1)) (_ bv1 32) member_0_result_7))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_8 _let_0)))) (= member_0_curr_9 (ite (and (and (and (and (and (and (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_8) member_0_val_1))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_8) member_0_curr_8)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_9 (ite (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_9 _let_0))) (= (select arr_val_15 member_0_curr_9) member_0_val_1)) (_ bv1 32) member_0_result_8))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_9 _let_0)))) (= member_0_curr_10 (ite (and (and (and (and (and (and (and (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_9) member_0_val_1))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_9) member_0_curr_9)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_10 (ite (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_9 _let_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_10 _let_0))) (= (select arr_val_15 member_0_curr_10) member_0_val_1)) (_ bv1 32) member_0_result_9))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_10 _let_0)))) (= member_0_curr_11 (ite (and (and (and (and (and (and (and (and (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_10) member_0_val_1))) (not (and (not (= member_0_curr_9 _let_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_10) member_0_curr_10)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_11 (ite (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_10 _let_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1))) (not (and (not (= member_0_curr_9 _let_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_11 _let_0))) (= (select arr_val_15 member_0_curr_11) member_0_val_1)) (_ bv1 32) member_0_result_10))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_11 _let_0)))) (= member_0_curr_12 (ite (and (and (and (and (and (and (and (and (and (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_11) member_0_val_1))) (not (and (not (= member_0_curr_10 _let_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 _let_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_11) member_0_curr_11)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_12 (ite (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_11 _let_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1))) (not (and (not (= member_0_curr_10 _let_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 _let_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_12 _let_0))) (= (select arr_val_15 member_0_curr_12) member_0_val_1)) (_ bv1 32) member_0_result_11))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_12 _let_0)))) (= member_0_curr_13 (ite (and (and (and (and (and (and (and (and (and (and (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_12) member_0_val_1))) (not (and (not (= member_0_curr_11 _let_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 _let_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 _let_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_12) member_0_curr_12)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_13 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_12 _let_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1))) (not (and (not (= member_0_curr_11 _let_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 _let_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 _let_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_13 _let_0))) (= (select arr_val_15 member_0_curr_13) member_0_val_1)) (_ bv1 32) member_0_result_12))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_13 _let_0)))) (= member_0_curr_14 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_13) member_0_val_1))) (not (and (not (= member_0_curr_12 _let_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 _let_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 _let_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 _let_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_13) member_0_curr_13)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_14 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_13 _let_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1))) (not (and (not (= member_0_curr_12 _let_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 _let_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 _let_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 _let_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_14 _let_0))) (= (select arr_val_15 member_0_curr_14) member_0_val_1)) (_ bv1 32) member_0_result_13))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= member_0_curr_14 _let_0)))) (= member_0_curr_15 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and _let_1 (= (select arr_val_15 member_0_curr_14) member_0_val_1))) (not (and (not (= member_0_curr_13 _let_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1)))) (not (and (not (= member_0_curr_12 _let_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 _let_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 _let_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 _let_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_1) (select arr_next_43 member_0_curr_14) member_0_curr_14)))))
(assert (let ((_let_0 (bvneg (_ bv1 32)))) (= member_0_result_15 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_14 _let_0)) (= (select arr_val_15 member_0_curr_14) member_0_val_1))) (not (and (not (= member_0_curr_13 _let_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1)))) (not (and (not (= member_0_curr_12 _let_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 _let_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 _let_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 _let_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (_ bv0 32) member_0_result_14))))
(assert (= main_0_x_1 member_0_result_15))
(check-sat-assuming ( (let ((_let_0 (bvneg (_ bv1 32)))) (let ((_let_1 (not (= (select arr_next_29 delete_0_head_1) _let_0)))) (let ((_let_2 (not (= member_0_curr_14 _let_0)))) (not (and (and (and (and (=> (bvult main_0_i_14 (_ bv13 32)) (not (bvult main_0_i_15 (_ bv13 32)))) (=> (and (= (select arr_val_15 delete_0_head_14) delete_0_val_1) _let_1) (not (= (select arr_val_15 delete_0_head_15) delete_0_val_1)))) (=> (and (not (= delete_0_curr_27 _let_0)) _let_1) (not (not (= delete_0_curr_29 _let_0))))) (=> (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and _let_2 (= (select arr_val_15 member_0_curr_14) member_0_val_1))) (not (and (not (= member_0_curr_13 _let_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1)))) (not (and (not (= member_0_curr_12 _let_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 _let_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 _let_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 _let_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 _let_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 _let_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 _let_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 _let_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 _let_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 _let_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 _let_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 _let_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) _let_2) (not (not (= member_0_curr_15 _let_0))))) (= main_0_x_1 (_ bv0 32))))))) ))
